Monus _∸_
is right adjoint to addition _+_
across usual _≤_
preorder
#1949
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Surprised that these properties are not already there; they may induce downstream a number of simplification to proofs of properties of monus. But not for this PR!
Separately, in view of the right->left direction of the adjunction: monus is defined as a total function
_-_
inAgda.Builtin.Nat
, and reimported as_∸_
... why don't we define an alternative functionn ∸ m
only on those arguments satisfyingm ≤ n
(by an easy recursion on the inductive definition of that relation; alternatively with an irrelevant instance argument of that type, and then simply definitionally equal toAgda.Builtin.Nat._-_
) and then prove the two definitions extensionally equal? The fact that_-_
has certain properties provable outright, without further ordering assumptions here or there, seems moot: the only ones which matter are those restricted to the partial domain... but our library setup doesn't typically take account for that. A case of strict(er) specification, but (more) permissive implementation?